\documentclass{llncs}

\usepackage{url}
\usepackage{fullpage}
\usepackage{proof}
\usepackage{amssymb}
\usepackage{latexsym}
\usepackage{xcolor}


\newcommand{\frank}[1]{\textcolor{blue}{\textbf{[#1 --Frank]}}}

\newcommand{\text}[1]{\mbox{#1}}
\newcommand{\wc}{\_}
\newcommand{\mulstep}{ \stackrel{*}{\leadsto}}
\newcommand{\lam}[2]{\lambda #1 . #2}
\newcommand{\evals}[2]{#1 \downarrow #2}

\newcommand{\wm}[0]{\stackrel{\textit{w}}{\to}}
\newcommand{\interp}[1]{[\negthinspace[#1]\negthinspace]}
\newcommand{\symm}[1]{\langle\textit{#1}\rangle}
\newcommand{\rrl}[1]{\textit{r-#1}}
\newcommand{\rrlb}[0]{\textit{r-}\beta}
\newcommand{\trl}[1]{\textit{t-#1}}
\begin{document}
%\pagestyle{empty}
\title{Lambda Encoding in Total Type Theory}
\author{Peng Fu}
\institute{Computer Science, The University of Iowa}
\date{Aug 21, 2012}


\maketitle
\thispagestyle{empty}
\begin{abstract}
This 
\end{abstract}



\section{Introduction}

\subsection{Lambda Calculus}



From Church, Curry to Howard's notion of construction \cite{dummy}

\subsection{Type Theory}
From Rusell to Today's Calculus of Construction

\subsection{Relation with Verification}

\subsection{Motivations}

\subsection{Overview}





\subsection{}

\subsection{}

\subsection{}

\section{Lambda Encoding}


\section{Type Theory}


\section{Paper Results I}

\subsection{Curry-Howard's Notion of Constructions}

\subsection{Russell's System}
\begin{definition}[Proof Terms]

\

\noindent $ \pi \ ::= \ \alpha \ | \ \lambda \alpha:F.\pi \ | \ \pi \pi'\ | \lambda x:T.\pi \ | \ \pi t $.

\end{definition}


\begin{definition}[Pseudo-Terms]

\

\noindent $t \ :: = \  \ x \ |  \ \lambda x.t \ | \ t t'  \ | \ t \supset t' \ | \ \forall x:T.t \ | \ t \wedge t' $



\end{definition}

\noindent Conventions: We use $M$ as metavariable for $t$ when we run out of ways to write pseudo-terms.

\begin{definition}[Formulaic Types]

\

\noindent $T \ :: =  \ \iota  \ | \ o \ | \ T \to o$
\end{definition}

\begin{definition}[Typing]

\

\begin{tabular}{lllll}
\infer{\Delta \vdash x:T}{(x:T) \in \Delta}

& & & &

\infer{\Delta \vdash \lambda x.t : T \to T' }{ \Delta, x:T \vdash t : T'}

\\

\\

\infer{\Delta \vdash t t': T} {\Delta \vdash t: T' \to T & \Delta \vdash t' : T'}

& & & &

\infer{\Delta \vdash \forall x:T.t : o}{ \Delta, x:T \vdash t : o & T \not = o}

\\

\\

\infer{\Delta \vdash t_1 \supset t_2: o}{ \Delta \vdash t_1 : o & \Delta \vdash t_1 : o}

& & & &

%% \infer{\Delta \vdash \exists x:T.F : \mathsf{Ok}}{ \Delta, x:T \vdash F : \mathsf{Ok}}

\\

\end{tabular}
\end{definition}

\noindent Convention: we call $t$ a formula if $\Delta \vdash t:o$, usually written as $F$. We call $t$ a term if $\Delta \vdash t:T$ where $T \not = o$, 
written as $t$.

\begin{definition}[Proofs Annotation]

\

\begin{tabular}{lllll}
\infer{\Delta, \Gamma \vdash \alpha:F} {(\alpha:F) \in \Gamma & \Delta \vdash F:o}

& & & &

\infer{\Delta, \Gamma \vdash \lambda \alpha:F_1.\pi: F_1 \supset F_2 }{ \Delta, \Gamma,\alpha:F_1 \vdash \pi:F_2 & \Delta \vdash F_1 \supset F_2:o}

\\

\\

\infer{\Delta, \Gamma \vdash \lambda x:T.\pi: \forall x:T.F }{\Delta,x:T, \Gamma \vdash \pi:F & \Delta,x:T \vdash F:o & x \notin FV(\Gamma)}

& & & &

\infer{\Delta, \Gamma \vdash \pi_1 \pi_2 : F_2}{\Delta, \Gamma \vdash \pi_1 : F_1 \supset F_2 & \Delta, \Gamma \vdash \pi_2 : F_1}

\\

\\

\infer{\Delta, \Gamma \vdash \pi t : [t/x]F}{\Delta, \Gamma \vdash \pi : \forall x:T.F & \Delta \vdash t : T}

& & & &


\\



\end{tabular}
\end{definition}


\begin{definition}[Formula Shape]
A pseudo-term $t$ is of formula shape iff $t$ is of the form $t_1 \wedge t_2$, $t_1 \supset t_2$ or $\forall x:T.t'$.
\end{definition}

\begin{lemma}[Shape Lemma I]
If $\Delta \vdash t:T_1 \to (T_2 \to (...  T'))$

\end{lemma}

\begin{lemma}[Shape Lemma II]
If $\Delta \vdash t:o$ and $t$ is not in formula shape, then $t$ is of the form: 

\noindent $(\lambda x_1...\lambda x_n . F M_1...M_m) t_1 t_2...t_n$ with $n \geq 0$ and $m \geq 0$. $\Delta, x_1:T_1,...,x_n:T_n \vdash F:o$ and $F$ is of the form $ x M_1...M_m \ | \ M \supset M' \ | \  \forall x:T.M$ with $m \geq 0$.

\end{lemma}

\begin{proof}
By induction on the derivation of $\Delta \vdash t:o$.

\

\noindent Base Case:

\

\infer{\Delta \vdash x:T}{(x:T) \in \Delta}

\

\noindent In this case, $n=m=0$. 

\

\noindent Step Case:

\

\infer{\Delta \vdash \forall x:T.t : o}{ \Delta, x:T \vdash t : o & T \not = o}

\

\noindent This case will not arise since $\forall x:T.t$ is of formula shape.

\

\noindent Step Case:

\

\infer{\Delta \vdash t_1 \supset t_2: o}{ \Delta \vdash t_1 : o & \Delta \vdash t_1 : o}

\

\noindent This case will not arise since $t_1 \supset t_2$ is of formula shape.

\

\noindent Step Case:

\

\infer{\Delta \vdash \lambda x.t : T \to T' }{ \Delta, x:T \vdash t : T'}

\

\noindent This case will not arise since $o \not = T \to T'$.

\

\noindent Step Case:

\

\infer{\Delta \vdash t t': T} {\Delta \vdash t: T' \to T & \Delta \vdash t' : T'}

\

\noindent In this case, $T = o$, $\Delta \vdash t: T' \to o$ and $\Delta \vdash t' : T'$.
By induction on the derivation of $\Delta \vdash t: T' \to o$:

\

If $t = y$, then $n = 0, m = 0$. 

\

If $\Delta, x:T' \vdash t'' : o$ and $\lambda x.t'' = t$, then we have the form $(\lambda x.F)t'$. So $n = 1$ and $m = 0$. 

\

If $\Delta \vdash t'' : T'' \to (T' \to o)$ and $\Delta \vdash t''':T''$ and $t = t'' t'''$. 




\end{proof}



\subsection{System F}
To obtain Girard's system F, which intuitively corresponds to higher order propositional logic. We drop the notion of term, and add formula variable 
and quantification over formula variables. And we add two proof terms to handle generalize/instantiation of formula variable.

\begin{definition}[Proof Terms]

\

\noindent $ \pi \ ::= \ \alpha \ | \ \lambda \alpha:F.\pi \ | \ \pi \pi'\ |  \ \pi F \ | \ \Lambda X.\pi$.

\end{definition}

\begin{definition}[Formulas]

\

\noindent $F \ :: = \ X \ | \ F \to F' \ | \ \forall X.F$

\end{definition}

\begin{definition}[Proofs Annotation]

\

\begin{tabular}{lllll}
\infer{\Gamma \vdash \alpha:F} {(\alpha:F) \in \Gamma }

& & & &

\infer{\Gamma \vdash \lambda \alpha:F_1.\pi: F_1 \to F_2 }{  \Gamma,\alpha:F_1 \vdash \pi:F_2 }

\\

\\

\infer{\Gamma \vdash \Lambda X.\pi: \forall X.F }{ \Gamma \vdash \pi:F & X \notin FV(\Gamma)}

& & & &

\infer{\Gamma \vdash \pi_1 \pi_2 : F_2}{\Gamma \vdash \pi_1 : F_1 \to F_2 & \Gamma \vdash \pi_2 : F_1}

\\

\\

\infer{ \Gamma \vdash \pi F' : [F'/X]F}{\Gamma \vdash \pi : \forall X.F }


\end{tabular}
\end{definition}

\noindent Alternatively, one can simply not use the formulaic type system. Adapting the polymorphic type system where $o$ is the only type symbol. The only rule for this polymorphic type system is $x:o$. The notion of well-formed formula and proof annotations remain unchanged. 

\subsection{System $F^{\omega}$}

\noindent To obtain Girard's system $F^{\omega}$, one simply add a type system with types $T \ ::= \ o \ | \ T \to T'$. Others remains unchanged. We can see
now $F^{\omega}$ not only allow quantification over formula, but also quantification over higher order 'formulaic predicate'(a kind of predicate that apply to formula yeilds a formula. etc.). 

\subsection{Martin-L\"of's Type Theory(Dependent Type)}

\noindent It is a bit hard to obtain Martin-L\"of's type theory, since we are going to allow formula to have the ability to quantify over the proofs. 
We adopt a new notion of term  $ t \ ::= \ x \ | \ \lambda x.t \ | \ t t' \ | \ t \pi \ | \ \lambda \alpha.t $. Pseudo-formula $F\ ::= \ t  \ | \ \forall \alpha:F.F$. Types $T \ ::= o \ | \ F \to o \ | \ F \to T$.

\begin{definition}[Formulaic Terms]

\

\begin{tabular}{lllll}
\infer{\Delta, \Gamma \vdash x:T}{(x:T) \in \Delta}

& & & &

\infer{\Delta, \Gamma \vdash \lambda x.t : T \to T' }{ \Delta, x:T, \Gamma \vdash t : T'}

\\

\\

\infer{\Delta, \Gamma \vdash t t': T} {\Delta , \Gamma\vdash t: T' \to T & \Delta, \Gamma \vdash t' : T'}

& & & &

\infer{\Delta , \Gamma\vdash \lambda \alpha.t : F \to T' }{ \Delta,\Gamma, \alpha:F \vdash t : T'}

\\

\\

\infer{\Delta , \Gamma\vdash t \pi: T} {\Delta, \Gamma \vdash t: F \to T & \Gamma \vdash \pi : F}

\\
\end{tabular}
\end{definition}


\begin{definition}[Well-Formed Formulas]

\

\begin{tabular}{lllll}
\infer{\Delta, \Gamma \vdash t : \mathsf{wff}} {\Delta, \Gamma \vdash t : o}

& & & &

\infer{\Delta, \Gamma \vdash \forall \alpha:F.F : \mathsf{wff}}{ \Delta, \Gamma, \alpha:F \vdash F : \mathsf{wff}}

\\


\end{tabular}
\end{definition}

\begin{definition}[Proofs Annotation]

\

\begin{tabular}{lllll}
\infer{\Delta, \Gamma \vdash \alpha:F} {(\alpha:F) \in \Gamma & \Delta,\Gamma \vdash F:\mathsf{wff}}

& & & &

\infer{\Delta, \Gamma \vdash \lambda \alpha:F'.\pi: \forall \alpha:F'.F }{\Delta, \Gamma,\alpha:F' \vdash \pi:F }


\\

\\

\infer{\Delta, \Gamma \vdash \pi \pi' : [\pi'/\alpha]F}{\Delta, \Gamma \vdash \pi : \forall \alpha:F'.F & \Delta,\Gamma \vdash \pi' : F'}


\end{tabular}
\end{definition}

\noindent In order to maintain a degree of independency of terms and proof terms, we have to extend our notion of terms to allow applying them to proof terms. 
\subsection{Church's System}

\subsection{Applications}




\section{Paper Results II}

\section{Implementation}


\section{Conclusions and Future Work}



\bibliographystyle{plain}
\bibliography{comp}

\appendix

\section{Proofs}


\end{document}
